Definition

Denote by 𝚔𝚂𝙰𝚃\mathtt{kSAT} the language of all satisfiable kkCNF formulae.

(Denote by 𝟹𝚂𝙰𝚃\mathtt{3SAT} the language of all satisfiable 3CNF formulae.)

(see SAT problem)

Notes

  • 𝟹𝚂𝙰𝚃∈\mathtt{3SAT} \in NP
  • 𝟹𝚂𝙰𝚃∈\mathtt{3SAT} \in PSPACE
  • 𝟹𝚂𝙰𝚃\mathtt{3SAT} is NP-complete
    • (and in fact for k≥3k \geq 3)
  • SAT reduces to 𝟹𝚂𝙰𝚃\mathtt{3SAT} in polynomial time, i.e. 𝚂𝙰𝚃≤p𝟹𝚂𝙰𝚃\mathtt{SAT} \leq_p \mathtt{3SAT}
  • it is a simple example of a constraint satisfaction problem
  • 2SAT can be solved in O(n+m)O(n+m) for nn variables, mm clauses
    • can use implicative normal form (where e.g. a∨ba \lor b is equivalent to ¬a⇒b∧¬b⇒a\lnot a \Rightarrow b \land \lnot b \Rightarrow a) to construct directed graph of implications

References

  1. S. Arora, B. Barak. Computational Complexity: A Modern Approach, Cambridge University Press, 2009, pp. 45, 81-82.
  2. https://cstheory.stackexchange.com/questions/7213/direct-sat-to-3-sat-reduction
  3. https://ocw.mit.edu/courses/6-045j-automata-computability-and-complexity-spring-2011/567d75f927ca3c11a819baee9ab260ac_MIT6_045JS11_lec16.pdf
  4. https://cse.iitkgp.ac.in/~palash/2018AlgoDesignAnalysis/SAT-3SAT.pdf
  5. https://cp-algorithms.com/graph/2SAT.html